package logica;

import java.util.ArrayList;
import java.util.List;

import logica.CalculoProposicional.Operador;
import util.Tupla;

public class InterpretadorDeFormula 
{
	private CalculoProposicional calculoProposicional;
	
	/** Cria um interpretador de expressões, baseado nas propriedades especificadas no Calculo Proposicional especificado. */
	public InterpretadorDeFormula(CalculoProposicional calculo)
	{
		this.calculoProposicional = calculo;
	}
	
	/** Interpreta a expressão passada e gera uma formula proposicional correspondente. 
	 * @throws Exception */
	public Formula interpretar(String exp) throws Exception
	{
		exp = exp.trim();
		
		if(exp.length() == 0) throw new Exception("Expressão vazia!");
		
		List<Tupla<Formula, Operador>> termosAchados = new ArrayList<Tupla<Formula,Operador>>();

		while(exp.length() > 0)
		{
			if(comecaComParenteses(exp))
			{
				if(exp.length() < 2) //tem algo mais alem do parentese?
					throw new Exception("Esperado um fecha-parenteses, mas trecho acaba antes! Trecho: \""+exp+"\"");
				
				exp = exp.substring(1).trim(); //pego o que esta logo apos o '('
				try
				{
					int i = indiceFechaParentesisCorrespondente(exp);
					Formula ff = interpretar(exp.substring(0, i)); //interpreta a formula dentro dos parenteses
					exp = exp.substring(i+1).trim(); //pego o que vem depois do ')', sem espaços desnecessarios
					if(exp.length() > 0) //tem algo mais depois de um termo entre parenteses?
					{
						if(comecaComOperadorBinario(exp)) //se tiver, deve ser um operador
						{
							Operador operador = operadorBinarioNoIncioDe(exp);
							int op_str_size = calculoProposicional.conectivosLogicos.get(operador).length(); //pego o numero de caracteres do conectivo achado
							termosAchados.add(new Tupla<Formula, Operador>(ff, operador));//colocamos na lista de termos do mesmo nivel

							exp = exp.substring(op_str_size);//pego o que vem apos o operador, pulando
							//apos isso, volta para o loop para achar outros termos no mesmo nivel
						}
						else throw new Exception("Esperado um operador binário! Trecho: \""+exp+"\""); //caso contrario esta errado
					}
					else //exp terminou com uma expressao entre parenteses
						termosAchados.add(new Tupla<Formula, Operador>(ff, null)); //colocamos na lista de termos do mesmo nivel, sem operador pois é o ultimo
				}
				catch(Exception e)
				{
					throw new Exception("Problema ao procurar fecha-parenteses. Trecho: \""+exp+"\"\n"+e.getMessage());
				}
			}
			
			else if(serAtomo(exp.charAt(0)))
			{
				Character atomo = exp.charAt(0);
				FormulaAtomica ff = new FormulaAtomica(calculoProposicional, atomo);
				exp = exp.substring(1).trim(); //pego o que vem depois do atomo, sem espaços desnecessarios
				
				if(exp.length() > 0) //tem algo mais depois de um atomo?
				{
					if(comecaComOperadorBinario(exp)) //se tiver, deve ser um operador
					{
						Operador operador = operadorBinarioNoIncioDe(exp);
						int op_str_size = calculoProposicional.conectivosLogicos.get(operador).length(); //pego o numero de caracteres do conectivo achado
						termosAchados.add(new Tupla<Formula, Operador>(ff, operador));//colocamos na lista de termos do mesmo nivel

						exp = exp.substring(op_str_size);//pego o que vem apos o operador, pulando
						//apos isso, volta para o loop para achar outros termos no mesmo nivel
					}
					else throw new Exception("Esperado um operador binário! Trecho: \""+exp+"\""); //caso contrario esta errado
				}
				else //exp terminou com uma expressao entre parenteses
					termosAchados.add(new Tupla<Formula, Operador>(ff, null)); //colocamos na lista de termos do mesmo nivel, sem operador pois é o ultimo
			}
			else if(comecaComNegacao(exp))
			{
				int neg_str_size = calculoProposicional.conectivosLogicos.get(Operador.NEGACAO).length(); //pego o numero de caracteres do conectivo da negação
				exp = exp.substring(neg_str_size); //pula o simbolo de negacao
				int i = indiceProximoOperadorPrecedenciaInferiorANegacao(exp);
				Formula ff = new FormulaNegacao(calculoProposicional, interpretar(exp.substring(0, i) )); //crio a formula como a negacao do que está entre 0 e i
				exp = exp.substring(i).trim(); //pego o que vem depois do escopo da negacao, sem espaços desnecessarios
				
				if(exp.length() > 0) //tem algo mais depois do escopo da negacao?
				{
					if(comecaComOperadorBinario(exp)) //se tiver, deve ser um operador
					{
						Operador operador = operadorBinarioNoIncioDe(exp);
						int op_str_size = calculoProposicional.conectivosLogicos.get(operador).length(); //pego o numero de caracteres do conectivo achado
						termosAchados.add(new Tupla<Formula, Operador>(ff, operador));//colocamos na lista de termos do mesmo nivel
						
						exp = exp.substring(op_str_size);//pego o que vem apos o operador
						//apos isso, volta para o loop para achar outros termos no mesmo nivel
					}
					else throw new Exception("Esperado um operador binário! Trecho: \""+exp+"\""); //caso contrario esta errado
				}
				else //exp terminou com uma expressao entre parenteses
					termosAchados.add(new Tupla<Formula, Operador>(ff, null)); //colocamos na lista de termos do mesmo nivel, sem operador pois é o ultimo
			}
			
			exp = exp.trim();
		}
		
		return arrumaTermosPorPrecedencia(termosAchados);
	}
	
	/** Retorna o indice do fecha parenteses correspondente ao nivel atual de escopo. O abre parentese deve estar omitido. 
	 * @throws Exception Quando não acha o parentese correspondente*/
	private static
	int indiceFechaParentesisCorrespondente(String subexp) throws Exception
	{
		int count=0;
		char[] array = subexp.toCharArray();
		for(int i = 0; i < array.length; i++)
		{
			if(array[i] == '(')
				count++;
			
			else if(array[i] == ')')
			{
				if(count == 0) return i;
				else count--;
			}	
		}
		throw new Exception("Indice nao encontrado!");
	}
	
	/** Retorna true se o a expressão em exp começa com parentesis. 
	 * Verifica se o primeiro caractere em exp é '('.
	 * Ou seja, se o primeiro caractere de exp for espaço (o caractere ' '), esse método retornará false */
	private static 
	boolean comecaComParenteses(String exp)
	{
		return exp.charAt(0) == '(';
	}
	
	/** Retorna true se a expressão exp começa com o operador negação. */
	private
	boolean comecaComNegacao(String exp)
	{
		String negacao_str = calculoProposicional.conectivosLogicos.get(Operador.NEGACAO); //pego o conectivo de negação
		return exp.startsWith(negacao_str);
	}
	
	/** Caso a expressão exp comece com um operador, retorna true. Caso contrário retorna false. */
	private 
	boolean comecaComOperadorBinario(String exp)
	{
		if(operadorBinarioNoIncioDe(exp) == null) return false;
		else return true;
	}
	
	/** Retorna o operador no inicio da expressao exp. Caso não reconheça algum, retorna null. */
	private 
	Operador operadorBinarioNoIncioDe(String exp)
	{
		for(Operador operador : calculoProposicional.conectivosLogicos.keySet())
		{
			String conectivo = calculoProposicional.conectivosLogicos.get(operador);
			if(exp.startsWith(conectivo))
				return operador;
		}
		
		return null;
	}
	
	/** Verifica se o caratere passado é um simbolo proposicional válido. */
	private 
	boolean serAtomo(char ch)
	{
		for(Atomo a : calculoProposicional.simbolosProposicionais)
			if(a.rotulo.equals(Character.toString(ch))) 
				return true;
		
		return false;
	}
	
	/** Acha o indice do proximo operador em exp com precedencia inferior a da negação. */
	private int indiceProximoOperadorPrecedenciaInferiorANegacao(String exp)
	{
		String str = exp;
		a: do
		{
			for(Operador op : calculoProposicional.conectivosLogicos.keySet())
			{
				String conectivo = calculoProposicional.conectivosLogicos.get(op);
				if(str.startsWith(conectivo))
				{
					break a;
				}
			}
			if(str.charAt(0) == '(') //verifico parentese
			{
				int contaParenteses = 1;
				do
				{
					str = str.substring(1);
					if(str.charAt(0) == '(') contaParenteses++;
					else if(str.charAt(0) == ')') contaParenteses--;
					
				}while(contaParenteses != 0);
				
			}
			str = str.substring(1);
		}
		while(str.length() > 0);
		
		return exp.length()-str.length();
	}
	
	/** Retorna uma formula com os termos em mesmo nivel aninhados por precedencia. */
	private Formula arrumaTermosPorPrecedencia(List<Tupla<Formula, Operador>> termos) throws Exception
	{
		return arrumaTermosPorPrecedencia(termos, Operador.EQUIVALENCIA); //começaremos pela equivalencia
	}
	
	/** Retorna uma formula com os termos em mesmo nivel ajustados apenas pela precedencia do operador especificado.
	 * Este método faz chamadas recursivas com precedencias cada vez maiores até os termos ficarem corretamente aninhados. */
	private Formula arrumaTermosPorPrecedencia(List<Tupla<Formula, Operador>> termos, Operador operacaoPrecedente) throws Exception
	{
		Formula formulaAnterior = null;
		
		if(operacaoPrecedente == Operador.CONJUNCAO) // se for conjuncao, ja esta limpo de todos os outros termos menos precedentes
		{
			for(Tupla<Formula, Operador> tupla : termos)
			{
				if(formulaAnterior == null)
				{
					formulaAnterior = tupla.termo1;
				}
				else
				{
					Formula f = new FormulaConjuncao(calculoProposicional, formulaAnterior, tupla.termo1);
					formulaAnterior = f;
				}
			}
			return formulaAnterior;
		}
		
		//se nao for conjuncao, vamos descobrir que sera o cara mais precedente apos o atual
		Operador proximaOperacaoPrecedente = null;
		switch(operacaoPrecedente)
		{
			case EQUIVALENCIA:
				proximaOperacaoPrecedente = Operador.IMPLICACAO;
				break;
			case IMPLICACAO:
				proximaOperacaoPrecedente = Operador.DISJUNCAO;
				break;
			case DISJUNCAO:
				proximaOperacaoPrecedente = Operador.CONJUNCAO;
				break;
			default:
				break;
		}
		
		for(int i = 0, a = 0; i < termos.size(); i++)
		{
			if(termos.get(i).termo2 == operacaoPrecedente)
			{
				List<Tupla<Formula, Operador>> sublista = termos.subList(a, i+1);
				sublista.get(i-a).termo2 = null;
				
				Formula f = arrumaTermosPorPrecedencia(sublista, proximaOperacaoPrecedente);
				
				if(formulaAnterior == null)
				{
					formulaAnterior = f;
				}
				else
				{
					Formula ff = instanciaDeAcordoComOperador(operacaoPrecedente, formulaAnterior, f);
					formulaAnterior = ff;
				}
				
				a = i+1;
			}
			else if(termos.get(i).termo2 == null) // chegamos no fim da lista de termos, hora de finalizar
			{
				List<Tupla<Formula, Operador>> sublista = termos.subList(a, i+1);
				
				Formula f = arrumaTermosPorPrecedencia(sublista, proximaOperacaoPrecedente);
				
				if(formulaAnterior == null) // nao teve nenhum termo encotrado antes da operacao
				{
					return f;
				}
				else
				{
					Formula ff = instanciaDeAcordoComOperador(operacaoPrecedente, formulaAnterior, f);
					return ff;
				}
			}
		}
		throw new Exception("Erro ao organizar precedencia!");
	}
	
	/** Cria uma instancia correta de acordo com o operador */
	private
	Formula instanciaDeAcordoComOperador(Operador operador, Formula termo1, Formula termo2)
	{
		switch(operador)
		{
			case EQUIVALENCIA:
				return new FormulaEquivalencia(calculoProposicional, termo1, termo2);

			case IMPLICACAO:
				return new FormulaImplicacao(calculoProposicional, termo1, termo2);

			case DISJUNCAO:
				return new FormulaDisjuncao(calculoProposicional, termo1, termo2);
				
			case CONJUNCAO: //nao deveria chegar também
				return new FormulaConjuncao(calculoProposicional, termo1, termo2);

			default: //nao deveria chegar aqui...
				System.err.println("Algo errado ao interpretar. Operacao "+operador.name()+" precedente indevida! Apenas operações binarias são esperadas nessa funcão!");
				return null;
		}
	}

}
